(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 3))
(let ((e4 (- v1)))
(let ((e5 (/ e3 (- e3))))
(let ((e6 (- v0 v2)))
(let ((e7 (> e4 e4)))
(let ((e8 (>= v1 v2)))
(let ((e9 (< e4 e5)))
(let ((e10 (< v1 e5)))
(let ((e11 (= e6 v1)))
(let ((e12 (= v0 v2)))
(let ((e13 (<= v1 e6)))
(let ((e14 (= v1 e5)))
(let ((e15 (= v2 v2)))
(let ((e16 (>= v2 e6)))
(let ((e17 (= e4 e6)))
(let ((e18 (> v2 v2)))
(let ((e19 (>= v0 e4)))
(let ((e20 (not e13)))
(let ((e21 (xor e15 e12)))
(let ((e22 (= e17 e14)))
(let ((e23 (or e7 e22)))
(let ((e24 (and e21 e8)))
(let ((e25 (xor e16 e11)))
(let ((e26 (=> e25 e20)))
(let ((e27 (= e18 e23)))
(let ((e28 (and e24 e26)))
(let ((e29 (and e27 e9)))
(let ((e30 (=> e19 e19)))
(let ((e31 (or e10 e28)))
(let ((e32 (and e30 e29)))
(let ((e33 (and e32 e31)))
e33
))))))))))))))))))))))))))))))))

;; CHECK: (assert (= v0 (/ (- 12) (- 85))))
;; CHECK: (assert (= v2 (/ 59 11)))
;; CHECK: (check-sat)
(check-sat-assuming-model (v0 v2) ((/ (- 12) (- 85)) (/ 59 11)))
